\begin{tabbing}
$\forall$$i$, $a$, $x$:Id, $A$, $T$:Type, $P$:($A$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]@$i$: ma{-}single{-}pre1($x$;$A$;$a$;$T$;$x$,$v$.$P$($x$,$v$)) $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: ma{-}single{-}pre1($x$;$A$;$a$;$T$;$x$,$v$.$P$($x$,$v$)) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]vartype($i$;$x$) $\subseteq\rho$ $A$
\\[0ex]\& ($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ kind($e$) $=$ locl($a$) $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id
\\[0ex]$\Rightarrow$ \=(kind($e$) $=$ locl($a$) $\in$ Knd $\Rightarrow$ $P$($x$ when $e$,val($e$)))\+
\\[0ex]\& (\=$\exists$${\it e'}$:E.\+
\\[0ex]($e$ $<$loc ${\it e'}$) $\vee$ $e$ $=$ ${\it e'}$ $\in$ E
\\[0ex]\& kind(${\it e'}$) $=$ locl($a$) $\in$ Knd $\vee$ ($\forall$$v$:$T$. $\neg$$P$(($x$ after ${\it e'}$),$v$)))))
\-\-\-\-\-
\end{tabbing}